/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ ∧/THE PROGRAMMING LANGUAGE ELEPHANT

␈↓ α∧␈↓␈↓ ελby John McCarthy

␈↓ α∧␈↓␈↓ αTThe␈α∪Elephant␈α∪(it␈α∪never␈α∀forgets)␈α∪programming␈α∪language␈α∪does␈α∪assignment␈α∀by␈α∪regarding
␈↓ α∧␈↓variables␈αas␈αexplicit␈αfunctions␈αof␈αtime;␈αe.g.␈αwhere␈αAlgol␈αexpects␈α␈↓↓x␈α:=␈↓,␈αElephant␈αexpects␈α␈↓↓x(t)␈α=␈↓.␈α The
␈↓ α∧␈↓program␈α⊂counter␈α∂is␈α⊂also␈α∂explicitly␈α⊂regarded␈α∂as␈α⊂a␈α∂function␈α⊂of␈α∂time.␈α⊂ Overcoming␈α⊂the␈α∂inhibition
␈↓ α∧␈↓against␈α∂explicit␈α⊂use␈α∂of␈α⊂time␈α∂as␈α⊂the␈α∂independent␈α∂variable␈α⊂allows␈α∂programs␈α⊂to␈α∂be␈α⊂represented␈α∂as
␈↓ α∧␈↓collections␈α
of␈α
sentences␈αin␈α
a␈α
first␈αorder␈α
logical␈α
language␈α
that␈αcan␈α
be␈α
used␈αto␈α
prove␈α
properties␈αof␈α
the
␈↓ α∧␈↓program.␈α∪ Moreover,␈α∩allowing␈α∪the␈α∩right␈α∪hand␈α∩sides␈α∪of␈α∩equations␈α∪to␈α∩refer␈α∪to␈α∩other␈α∪than␈α∩the
␈↓ α∧␈↓immediate␈αpast␈αallows␈α"high␈αlevel"␈αprograms␈αthat␈αdon't␈αrequire␈αdata␈αstructure␈αdefinitions␈αrequired
␈↓ α∧␈↓by␈α∞ordinary␈α∞programming␈α∞languages.␈α∞ The␈α∞concepts␈α∞are␈α∞best␈α∞understood␈α∞by␈α∞means␈α∞of␈α
examples.
␈↓ α∧␈↓The notation is as in (Cartwright and McCarthy 1979).

␈↓ α∧␈↓Example

␈↓ α∧␈↓1 - Translating a sequential program into Elephant

␈↓ α∧␈↓␈↓ αTConsider␈α⊂the␈α⊃following␈α⊂Algol␈α⊃60␈α⊂program␈α⊃fragment␈α⊂(declarations␈α⊃are␈α⊂omitted)␈α⊃for␈α⊂doing
␈↓ α∧␈↓multiplication by addition:

␈↓ α∧␈↓↓␈↓ αTi := n;␈↓ εt0
␈↓ α∧␈↓↓␈↓ αTp := 0;␈↓ εt1
␈↓ α∧␈↓↓loop:   ␈↓αif␈↓↓ i = 0 ␈↓αthen␈↓↓ ␈↓αgo to␈↓↓ done;␈↓ εt2
␈↓ α∧␈↓↓␈↓ αTi := i - 1;␈↓ εt3
␈↓ α∧␈↓↓␈↓ αTp := p + m;␈↓ εt4
␈↓ α∧␈↓↓␈↓ αT␈↓αgo to␈↓↓ loop;␈↓ εt5
␈↓ α∧␈↓↓done:␈↓ εt6

␈↓ α∧␈↓The corresponding Elephant program consists of the equations

␈↓ α∧␈↓↓pc(0) = 0,

␈↓ α∧␈↓↓∀t.[t > 0 ⊃ i(t) ␈↓ βj= ␈↓ ∧∧IF pc(t - 1) = 0 THEN n
␈↓ α∧␈↓↓␈↓ ∧∧ELSE IF pc(t - 1) = 3 THEN i(t-1) - 1
␈↓ α∧␈↓↓␈↓ ∧∧ELSE i(t-1)],

␈↓ α∧␈↓↓∀t.[t > 0 ⊃ p(t) ␈↓ βj= ␈↓ ∧∧IF pc(t - 1) = 1 THEN 0
␈↓ α∧␈↓↓␈↓ ∧∧ELSE IF pc(t-1) = 4 THEN p(t-1) + m
␈↓ α∧␈↓↓␈↓ ∧∧ELSE p(t-1)],

␈↓ α∧␈↓↓␈↓and␈↓↓

␈↓ α∧␈↓↓∀t.[t > 0 ⊃ pc(t) ␈↓ βj= ␈↓ ∧∧IF pc(t-1) = 2 ∧ i(t-1) = 0 THEN 6
␈↓ α∧␈↓↓␈↓ ∧∧ELSE IF pc(t-1) = 5 THEN 2
␈↓ α∧␈↓↓␈↓ ∧∧ELSE pc(t-1) + 1].

␈↓ α∧␈↓␈↓ αTIn␈α∂these␈α∂equations␈α∂␈↓↓i(t)␈↓␈α∂and␈α∂␈↓↓p(t)␈↓␈α∂replace␈α∞the␈α∂simple␈α∂variables␈α∂of␈α∂the␈α∂Algol␈α∂program.␈α∞ The
␈↓ α∧␈↓function␈α⊃␈↓↓pc(t)␈↓␈α⊂is␈α⊃the␈α⊂program␈α⊃counter,␈α⊂and␈α⊃it␈α⊃takes␈α⊂values␈α⊃from␈α⊂1␈α⊃to␈α⊂6,␈α⊃corresponding␈α⊃to␈α⊂the
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓numbers␈αwritten␈αon␈α
the␈αright␈αof␈α
the␈αAlgol␈αprogram.␈α
 It␈αshould␈αbe␈α
apparent␈αfrom␈αthe␈αexample␈α
that
␈↓ α∧␈↓any␈αprogram␈αmade␈αup␈αof␈αassignments␈α
and␈α␈↓αgo to␈↓s␈αcan␈αbe␈αsystematically␈αtranslated␈αto␈α
an␈αElephant
␈↓ α∧␈↓program.␈α⊂ Notice␈α⊂also␈α⊂that␈α⊂the␈α∂length␈α⊂of␈α⊂the␈α⊂Elephant␈α⊂program␈α∂is␈α⊂linear␈α⊂in␈α⊂the␈α⊂length␈α⊂of␈α∂the
␈↓ α∧␈↓original␈α∀program.␈α∀ Having␈α∪one␈α∀value␈α∀of␈α∀␈↓↓pc(t)␈↓␈α∪for␈α∀each␈α∀statement␈α∪in␈α∀the␈α∀Algol␈α∀program␈α∪is
␈↓ α∧␈↓unnecessary,␈α
although␈α
it␈α
makes␈α
the␈α
systematic␈α
character␈α
of␈α
the␈α
translation␈α
more␈α
apparent.␈α
 If␈αwe␈α
let
␈↓ α∧␈↓␈↓↓pc(t) = 0␈↓␈αcorrespond␈α
to␈αthe␈α
initialization,␈α␈↓↓pc(t) = 1␈↓␈α
correspond␈αto␈α
the␈αloop,␈α
and␈α␈↓↓pc(t) = 2␈↓␈α
correspond
␈↓ α∧␈↓to the label ␈↓↓done,␈↓ then the equations become

␈↓ α∧␈↓↓pc(0) = 0,

␈↓ α∧␈↓↓∀t.[t > 0 ⊃ i(t)␈↓ βT=␈↓ ∧∧IF pc(t - 1) = 0 THEN n
␈↓ α∧␈↓↓␈↓ ∧∧ELSE IF pc(t - 1) = 1 ∧ i(t-1) ≠ 0 THEN i(t-1) - 1
␈↓ α∧␈↓↓␈↓ ∧∧ELSE i(t-1)],

␈↓ α∧␈↓↓∀t.[t > 0 ⊃ p(t)␈↓ βT=␈↓ ∧∧IF pc(t - 1) = 0 THEN 0
␈↓ α∧␈↓↓␈↓ ∧∧ELSE IF pc(t-1) = 1 ∧ i(t-1) ≠ 0 THEN p(t-1) + m
␈↓ α∧␈↓↓␈↓ ∧∧ELSE p(t-1)],

␈↓ α∧␈↓↓␈↓and␈↓↓

␈↓ α∧␈↓↓∀t.[t > 0 ⊃ pc(t)␈↓ βT=␈↓ ∧∧IF pc(t-1) = 1 ∧ i(t-1) = 0 THEN 2
␈↓ α∧␈↓↓␈↓ ∧∧ELSE pc(t-1) + 1].

␈↓ α∧␈↓␈↓ αTThe correctness of the original Elephant program is given by the sentence

␈↓ α∧␈↓␈↓ αT␈↓↓∀m n ∃t.[pc(t) = 6 ∧ p(t) = mn]␈↓,

␈↓ α∧␈↓while␈α∀the␈α∪modified␈α∀program␈α∪would␈α∀have␈α∀the␈α∪same␈α∀correctness␈α∪condition␈α∀except␈α∀for␈α∪having
␈↓ α∧␈↓␈↓↓pc(t) = 2␈↓␈αinstead␈αof␈α
␈↓↓pc(t) = 6.␈↓␈αEither␈αstatement␈α
is␈αprovable␈αfrom␈α
the␈αany␈αfirst␈αorder␈α
axiomatization
␈↓ α∧␈↓of␈α∀arithmetic␈α∀together␈α∀with␈α∀the␈α∀sentences␈α∀constituting␈α∀the␈α∀program.␈α∀ No␈α∀special␈α∀axioms␈α∪for
␈↓ α∧␈↓programs are required.

␈↓ α∧␈↓␈↓ αTThus␈α
an␈α
entirely␈α
conventional␈α
mathematical␈α
way␈α
of␈α
writing␈α
recursion␈α
equations␈α
leads␈α∞to␈α
a
␈↓ α∧␈↓convenient␈α∂programming␈α∂language.␈α∞ I␈α∂am␈α∂tempted␈α∂to␈α∞call␈α∂the␈α∂language␈α∞Algol␈α∂50,␈α∂since␈α∂it␈α∞could
␈↓ α∧␈↓easily have been developed at that time.

␈↓ α∧␈↓␈↓ αTThe␈α
actual␈α
proof␈α
in␈α
this␈α
case␈α
is␈α
misleadingly␈α
simple,␈α
since␈α
it␈α
is␈α
easy␈α
to␈α
write␈α
down␈αan␈α
explicit
␈↓ α∧␈↓formulas␈α
for␈α␈↓↓i(t),␈↓␈α
␈↓↓p(t),␈↓␈α
and␈α␈↓↓pc(t)␈↓␈α
and␈α
prove␈αthem␈α
by␈α
mathematical␈αinduction.␈α
 More␈αtypical␈α
proofs
␈↓ α∧␈↓occur␈α
when␈αit␈α
isn't␈α
convenient␈αto␈α
give␈α
explicit␈αformulas␈α
for␈αthe␈α
variables␈α
as␈αfunctions␈α
of␈α
time␈αor
␈↓ α∧␈↓for␈α
the␈α
value␈α
of␈α
␈↓↓t␈↓␈α
for␈α
which␈α
the␈α
program␈α
terminates.␈α
 Then␈α
the␈α
computational␈α
content␈α
of␈αthe␈α
proof
␈↓ α∧␈↓is␈αmay␈α
be␈αessentially␈α
the␈αsame␈α
as␈αthat␈α
of␈αan␈α
␈↓↓inductive␈αassertions␈↓␈α
proof␈αcombined␈α
with␈αinduction␈α
on
␈↓ α∧␈↓a rank function of the variables taking values in a suitable inductively ordered set.

␈↓ α∧␈↓Example

␈↓ α∧␈↓2 - Reversing a list

␈↓ α∧␈↓␈↓ αTReversing␈α⊂a␈α⊂list␈α⊃provides␈α⊂another␈α⊂example␈α⊃of␈α⊂an␈α⊂Elephant␈α⊂program␈α⊃and␈α⊂a␈α⊂proof␈α⊃of␈α⊂its
␈↓ α∧␈↓correctness.
␈↓ α∧␈↓␈↓ u3


␈↓ α∧␈↓↓␈↓ αTu := w;
␈↓ α∧␈↓↓␈↓ αTv := ␈↓NIL␈↓↓;
␈↓ α∧␈↓↓loop:   ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ ␈↓αgo to␈↓↓ done;
␈↓ α∧␈↓↓␈↓ αTv := [␈↓αa␈↓↓ u] . v;
␈↓ α∧␈↓↓␈↓ αTu := ␈↓αd␈↓↓ u;
␈↓ α∧␈↓↓␈↓ αT␈↓αgo to␈↓↓ loop;
␈↓ α∧␈↓↓done:

␈↓ α∧␈↓␈↓ αTThe corresponding Elephant program is
␈↓ α∧␈↓↓pc(0) = 0,

␈↓ α∧␈↓↓∀t.[t > 0 ⊃ u(t) ␈↓ βZ= ␈↓ βtIF pc(t-1) = 0 THEN w
␈↓ α∧␈↓↓␈↓ βtELSE IF pc(t-1) = 1 ∧ ¬null u(t-1) THEN ␈↓αd␈↓↓ u(t-1)
␈↓ α∧␈↓↓␈↓ βtELSE u(t-1)],

␈↓ α∧␈↓↓∀t.[t > 0 ⊃ v(t) ␈↓ βZ= ␈↓ βtIF pc(t-1) = 0 THEN ␈↓NIL␈↓↓
␈↓ α∧␈↓↓␈↓ βtELSE IF pc(t-1) = 1 ∧ ¬null u(t-1) THEN ␈↓αa␈↓↓ u(t-1) . v(t-1)
␈↓ α∧␈↓↓␈↓ βtELSE v(t-1)]

␈↓ α∧␈↓↓∀t.[t > 0 ⊃ pc(t) ␈↓ βZ= ␈↓ βtIF pc(t-1) = 1 ∧ ¬null u(t-1) THEN 1
␈↓ α∧␈↓↓␈↓ βtELSE pc(t-1) + 1].

␈↓ α∧␈↓␈↓ αTIn␈α
order␈αto␈α
give␈α
the␈αspecifications␈α
for␈αthis␈α
program,␈α
we␈αwill␈α
use␈αthe␈α
LISP␈α
program␈α␈↓↓reverse␈↓
␈↓ α∧␈↓defined by

␈↓ α∧␈↓␈↓ αT␈↓↓reverse u ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ reverse ␈↓αd␈↓↓ u * <␈↓αa␈↓↓ u>␈↓.

␈↓ α∧␈↓With␈α∂the␈α∂latter,␈α∂as␈α⊂shown␈α∂in␈α∂(Cartwright␈α∂and␈α∂McCarthy␈α⊂1979),␈α∂it␈α∂is␈α∂convenient␈α∂to␈α⊂prove␈α∂such
␈↓ α∧␈↓properties␈α⊗as␈α∃␈↓↓reverse reverse u = u␈↓␈α⊗and␈α∃␈↓↓reverse[u * v] = reverse v * reverse u␈↓.␈α⊗ The␈α⊗major␈α∃fact
␈↓ α∧␈↓about the Elephant program is expressed by

␈↓ α∧␈↓␈↓ αT␈↓↓∃t.(pc(t) = 2 ∧ v(t) = reverse w)␈↓.

␈↓ α∧␈↓It␈αcan␈αbe␈αproved␈αby␈αproving␈αthat␈α␈↓↓length␈αu(t)␈↓␈αis␈αa␈αdecreasing␈αfunction␈αof␈α␈↓↓t,␈↓␈αi.e.␈αfor␈αany␈α␈↓↓t␈↓␈αsuch␈αthat
␈↓ α∧␈↓␈↓↓pc(t) < 2,␈↓ there is ␈↓↓t' > t␈↓ such that ␈↓↓length u(t') < length t␈↓, and also that

␈↓ α∧␈↓␈↓ αT␈↓↓∀t.[reverse w = reverse u(t) * v(t)]␈↓.

␈↓ α∧␈↓This␈α∂is␈α∞just␈α∂an␈α∞␈↓↓inductive␈α∂assertions␈↓␈α∞proof.␈α∂ So␈α∞far␈α∂it␈α∞seems␈α∂that␈α∞the␈α∂our␈α∞Elephant␈α∂technique␈α∞of
␈↓ α∧␈↓proof␈α∩is␈α∪essentially␈α∩␈↓↓inductive␈α∩assertions␈↓,␈α∪and␈α∩is␈α∪less␈α∩flexible␈α∩than␈α∪the␈α∩technique␈α∪described␈α∩in
␈↓ α∧␈↓(Cartwright␈α
and␈α
McCarthy␈α
1979)␈α
that␈α
uses␈α
the␈α
␈↓↓functional␈α
equation␈↓␈α
and␈α
the␈α
␈↓↓minimization␈α
schema␈↓.
␈↓ α∧␈↓This␈α⊃is␈α⊂because␈α⊃␈↓↓inductive␈α⊂assertions␈↓␈α⊃provides␈α⊂no␈α⊃way␈α⊂of␈α⊃expressing␈α⊂algebraic␈α⊃relations␈α⊂among
␈↓ α∧␈↓functions defined by programs.

␈↓ α∧␈↓Non Algolic Elephant Programs

␈↓ α∧␈↓␈↓ αTWhen␈α∞we␈α∂translate␈α∞an␈α∞Algol␈α∂program␈α∞into␈α∞Elephant,␈α∂we␈α∞get␈α∞equations␈α∂in␈α∞which␈α∂the␈α∞␈↓↓x(t)␈↓s
␈↓ α∧␈↓depend␈αonly␈αon␈αthe␈α␈↓↓x(t-1)␈↓s.␈α However,␈αthe␈αrecursion␈αequations␈αwill␈αstill␈αhave␈αguaranteed␈αsolutions
␈↓ α∧␈↓if␈α∂the␈α∞␈↓↓x(t)␈↓s␈α∂depend␈α∞on␈α∂arbitrary␈α∞earlier␈α∂values␈α∂of␈α∞␈↓↓t.␈↓␈α∂This␈α∞leads␈α∂to␈α∞a␈α∂"high␈α∂level"␈α∞programming
␈↓ α∧␈↓language with the following features:
␈↓ α∧␈↓␈↓ u4


␈↓ α∧␈↓␈↓ αT1.␈α∞The␈α
program␈α∞refers␈α∞to␈α
the␈α∞past␈α
through␈α∞earlier␈α∞values␈α
of␈α∞␈↓↓t,␈↓␈α
just␈α∞as␈α∞though␈α
everything
␈↓ α∧␈↓were remembered.  That's why we call the language Elephant.

␈↓ α∧␈↓␈↓ αT2.␈α
The␈αcompiler␈α
is␈α
smart␈αand␈α
decides␈αwhat␈α
data␈α
structures␈αare␈α
required␈α
in␈αorder␈α
to␈αcarry␈α
out
␈↓ α∧␈↓the␈α
computations␈α
without␈α
remembering␈α
everything.␈α∞ To␈α
the␈α
extent␈α
that␈α
compilers␈α
can␈α∞be␈α
written
␈↓ α∧␈↓that␈α
do␈α
this␈α
effectively,␈αElephant␈α
is␈α
a␈α
"higher␈α
level"␈αlanguage␈α
in␈α
which␈α
the␈α
programer␈αspecifies␈α
less
␈↓ α∧␈↓than in Algol, etc.

␈↓ α∧␈↓Example

␈↓ α∧␈↓3 - An airline reservation system

␈↓ α∧␈↓␈↓ αTConsider␈α∃programming␈α∃a␈α⊗trivial␈α∃airline␈α∃reservation␈α∃system.␈α⊗ We␈α∃want␈α∃to␈α∃say␈α⊗that␈α∃␈↓↓a
␈↓ α∧␈↓↓passenger␈α∞has␈α
a␈α∞reservation␈α
if␈α∞he␈α
has␈α∞made␈α∞one␈α
that␈α∞has␈α
not␈α∞been␈α
cancelled␈↓.␈α∞ We␈α
do␈α∞not␈α∞want␈α
to
␈↓ α∧␈↓prescribe␈α∂what␈α⊂data␈α∂structures␈α∂have␈α⊂to␈α∂be␈α∂kept␈α⊂in␈α∂order␈α∂to␈α⊂be␈α∂able␈α∂to␈α⊂answer␈α∂the␈α⊂question␈α∂of
␈↓ α∧␈↓whether someone has a reservation.

␈↓ α∧␈↓␈↓ αTThis␈α∀program␈α∀replies␈α∀properly␈α∀to␈α∀requests␈α∀to␈α∀make␈α∀reservations,␈α∀cancel␈α∀them,␈α∀and␈α∪to
␈↓ α∧␈↓inquiries␈α⊂about␈α∂whether␈α⊂a␈α⊂reservation␈α∂exists.␈α⊂ The␈α∂program␈α⊂refers␈α⊂to␈α∂its␈α⊂input␈α∂in␈α⊂terms␈α⊂of␈α∂an
␈↓ α∧␈↓abstract␈α∀analytic␈α∀syntax␈α∀the␈α∀meaning␈α∀of␈α∀whose␈α∀mnemonic␈α∀predicate␈α∀and␈α∀function␈α∀names␈α∀is
␈↓ α∧␈↓hopefully␈αobvious.␈α The␈αonly␈αdata␈αstructure␈αexplicitly␈αmentioned␈αis␈αthe␈αnumber␈αof␈α
seats␈αcurrently
␈↓ α∧␈↓occupied,␈α
and␈α
even␈α
that␈α
could␈α
be␈αeliminated␈α
from␈α
the␈α
program.␈α
 The␈α
Elephant␈αcompiler,␈α
therefore,
␈↓ α∧␈↓gets␈αthe␈αhonor␈α
of␈αfiguring␈αout␈αwhat␈α
other␈αdata␈αstructures␈αare␈α
needed.␈α We␈αuse␈αthe␈α
convention␈αof
␈↓ α∧␈↓writing ␈↓↓{x}f␈↓ instead of ␈↓↓f(x)␈↓ when it is convenient to write the argument before the function name.

␈↓ α∧␈↓↓␈↓ αT∀t.[t > 0 ⊃ output(t) = {input(t-1)}[λ in.
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀IF ismake in THEN ␈↓ ¬Z[␈↓ ¬dIF hasrev(maker in,t) THEN "You had it"
␈↓ α∧␈↓↓␈↓ αT␈↓ ¬dELSE IF number(t) = N THEN "No room"
␈↓ α∧␈↓↓␈↓ αT␈↓ ¬dELSE "You have it now"]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE IF iscancel in THEN ␈↓ ¬Z[␈↓ ¬dIF hasrev(maker in,t) THEN "It's cancelled"
␈↓ α∧␈↓↓␈↓ αT␈↓ ¬dELSE "You don't have it to cancel"]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE IF isinquiry in THEN␈↓ ¬Z[␈↓ ¬dIF hasrev(maker in,t) THEN "You have one"
␈↓ α∧␈↓↓␈↓ αT␈↓ ¬dELSE "You don't have one"]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE ␈↓NIL␈↓↓]

␈↓ α∧␈↓↓␈↓ αT∀t.[t > 0 ⊃ number(t) = {input(t-1)}[λ in.
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀IF ismake in THEN ␈↓ ¬Z[␈↓ ¬dIF hasrev(maker in,t) ∨ number(t) = N THEN number(t)
␈↓ α∧␈↓↓␈↓ αT␈↓ ¬dELSE number(t) + 1]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE IF iscancel in THEN ␈↓ ¬Z[␈↓ ¬dIF hasrev(maker in,t) THEN number(t) - 1
␈↓ α∧␈↓↓␈↓ αT␈↓ ¬dELSE number(t)]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE number(t)]

␈↓ α∧␈↓where

␈↓ α∧␈↓␈↓ αT␈↓↓∀t.[hasrev(passenger,t)␈α∂≡␈α∂∃t1.(t1␈α∂<␈α∂t␈α∂∧␈α∂ismake␈α∞input␈α∂t1␈α∂∧␈α∂passenger␈α∂=␈α∂maker␈α∂input␈α∂t1␈α∞∧
␈↓ α∧␈↓↓number(t1) < N) ∧ ¬∃t2.(t1 < t2 < t ∧ iscancel input t2 ∧ maker input t2 = passenger))]␈↓.

␈↓ α∧␈↓␈↓ αTA␈α∞key␈α
difficulty␈α∞in␈α
making␈α∞a␈α∞compiler␈α
for␈α∞Elephant␈α
is␈α∞presented␈α
by␈α∞the␈α∞predicate␈α
␈↓↓hasrev.␈↓
␈↓ α∧␈↓The␈α⊂compiler␈α⊂has␈α⊂to␈α⊂understand␈α⊂that␈α∂it␈α⊂must␈α⊂remember␈α⊂successful␈α⊂reservations␈α⊂but␈α⊂can␈α∂forget
␈↓ α∧␈↓␈↓ u5


␈↓ α∧␈↓unsuccessful␈αattempts␈α
at␈αmaking␈αa␈α
reservation␈αand␈αthat␈α
it␈αcan␈αforget␈α
reservations␈αthat␈α
have␈αbeen
␈↓ α∧␈↓cancelled.␈α⊂ Perhaps␈α⊂␈↓↓hasrev␈↓␈α⊂should␈α⊂be␈α⊂written␈α∂using␈α⊂primitives␈α⊂that␈α⊂refer␈α⊂explicitly␈α⊂to␈α⊂the␈α∂most
␈↓ α∧␈↓recent occurrence of an event, and that this would permit a less intelligent compiler.

␈↓ α∧␈↓Example

␈↓ α∧␈↓4 Elephant program to count vertices in a list structure

␈↓ α∧␈↓␈↓ αTAnother␈αcontext␈αin␈αwhich␈αit␈αis␈αpossible␈αto␈αavoid␈αspecifying␈αa␈αdata␈αstructure␈αby␈αreferring␈αto
␈↓ α∧␈↓the␈α
past␈α
occurs␈α
when␈α
a␈α
list␈α
structure␈α
is␈αto␈α
be␈α
scanned.␈α
 The␈α
simplest␈α
example␈α
is␈α
a␈α
program␈αto␈α
count
␈↓ α∧␈↓the vertices in a list structure.

␈↓ α∧␈↓Here␈α␈↓↓a␈↓␈αis␈αthe␈αlist␈αstructure␈αbeing␈αscanned,␈α␈↓↓x␈↓␈αis␈αa␈αrunning␈αvariable␈αfor␈αthe␈αcurrent␈αstructure,␈αand␈α␈↓↓n␈↓
␈↓ α∧␈↓is the current count.

␈↓ α∧␈↓␈↓ αTBecause␈α∩of␈α∩Elephant's␈α∩ability␈α∩to␈α∩refer␈α∩to␈α∩the␈α∩past,␈α∩we␈α∩can␈α∩write␈α∩this␈α∩program␈α∩without
␈↓ α∧␈↓specifying␈αa␈αstack.␈α It␈αis␈αup␈αto␈αthe␈αcompiler␈αto␈αdecide␈αthat␈αa␈αstack␈αis␈αappropriate␈αfor␈αimplementing
␈↓ α∧␈↓the algorithm.
␈↓ α∧␈↓↓∀t.[t > 0 ⊃ x(t) ␈↓ βZ= ␈↓ βtIF pc(t-1) = 0 THEN a
␈↓ α∧␈↓↓␈↓ βtELSE IF pc(t-1) = 1 THEN
␈↓ α∧␈↓↓␈↓ ∧J[␈↓ ∧TIF [∀y.seen(y,t-1) ⊃ atom y ∨ seen(car y,t-1) ∧ seen(cdr y, t-1)]
␈↓ α∧␈↓↓␈↓ ¬TTHEN x(t-1)
␈↓ α∧␈↓↓␈↓ ∧TELSE IF ¬atom x(t-1) ∧ ¬seen(car x(t),t) then car x(t)
␈↓ α∧␈↓↓␈↓ ∧TELSE cdr x(mostrecent(t-1,λt1.¬seen(cdr(x(t1)),t-1)))]
␈↓ α∧␈↓↓␈↓ βtELSE x(t)]

␈↓ α∧␈↓↓∀t.[t > 0 ⊃ n(t) ␈↓ βZ= ␈↓ βtIF pc(t-1) = 0 THEN 0
␈↓ α∧␈↓↓␈↓ βtELSE IF␈↓ ¬∧pc(t-1) = 1
␈↓ α∧␈↓↓␈↓ ∧s∧␈↓ ¬∧¬[∀y.seen(y,t-1) ⊃ atom y ∨ seen(car y,t-1) ∧ seen(cdr y, t-1)]
␈↓ α∧␈↓↓␈↓ ¬TTHEN n(t-1) + 1
␈↓ α∧␈↓↓␈↓ βtELSE n(t-1)]

␈↓ α∧␈↓↓∀t.[t > 0 ⊃ pc(t) ␈↓ βZ= ␈↓ βtIF␈↓ ∧4pc(t-1) = 1
␈↓ α∧␈↓↓␈↓ ∧#∧␈↓ ∧4¬[∀y.seen(y,t-1) ⊃ atom y ∨ seen(car y,t-1) ∧ seen(cdr y, t-1)]
␈↓ α∧␈↓↓␈↓ ¬∧THEN 1
␈↓ α∧␈↓↓␈↓ βtELSE pc(t-1) + 1

␈↓ α∧␈↓where the predicate ␈↓↓seen␈↓ and the functional ␈↓↓mostrecent␈↓ are defined as follows:
␈↓ α∧␈↓↓∀y t.[seen(y,t) ≡ ∃t1.[t1 ≤ t ∧ y = x(t1)]]

␈↓ α∧␈↓↓∀t.[mostrecent(t, pred) = ␈↓αif␈↓↓ pred t ␈↓αthen␈↓↓ t ␈↓αelse␈↓↓ mostrecent(t - 1, pred)].

␈↓ α∧␈↓We␈α⊂would␈α⊂like␈α∂to␈α⊂regard␈α⊂these␈α⊂as␈α∂definitions␈α⊂not␈α⊂as␈α∂programs.␈α⊂ Indeed␈α⊂the␈α⊂compiled␈α∂program
␈↓ α∧␈↓shouldn't use them, but should do the job another way that uses time and space more efficiently.

␈↓ α∧␈↓Of course, this example is less perspicuous than the lisp program

␈↓ α∧␈↓␈↓↓count x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ count ␈↓αa␈↓↓ x + count ␈↓αd␈↓↓ x␈↓
␈↓ α∧␈↓␈↓ u6


␈↓ α∧␈↓which␈α
scans␈α
the␈α∞vertices␈α
in␈α
the␈α
same␈α∞order.␈α
 But␈α
then␈α
this␈α∞problem␈α
is␈α
especially␈α∞appropriate␈α
for
␈↓ α∧␈↓recursion and Lisp's built-in stack mechanism.

␈↓ α∧␈↓Most␈αlikely␈α
␈↓↓seen␈↓␈αand␈α
␈↓↓mostrecent␈↓␈αwill␈α
occur␈αin␈αother␈α
algorithms␈αwhere␈α
one␈αdoesn't␈α
want␈αto␈α
look␈αat
␈↓ α∧␈↓things that have been already tried.

␈↓ α∧␈↓Remarks:

␈↓ α∧␈↓1.␈α
Programs␈αin␈α
Lucid␈α(Ashcroft␈α
1974)␈αare␈α
also␈α
collections␈αof␈α
sentences␈αin␈α
a␈αfirst␈α
order␈αlanguage.␈α
 A
␈↓ α∧␈↓Lucid␈α∪object␈α∪is␈α∪a␈α∪vector␈α∪of␈α∪the␈α∪values␈α∪of␈α∪a␈α∪variable␈α∪throughout␈α∪time.␈α∪ This␈α∀permits␈α∪some
␈↓ α∧␈↓statements␈α
to␈αbe␈α
made␈αin␈α
a␈αvery␈α
neat␈αway.␈α
 However,␈α
it␈αseems␈α
to␈αbe␈α
less␈αflexible␈α
than␈αthe␈α
Elephant
␈↓ α∧␈↓device␈α
of␈α
admitting␈αthe␈α
time␈α
as␈αan␈α
explicit␈α
parameter.␈α Lucid␈α
program␈α
do␈αnot␈α
admit␈α
␈↓αgo to␈↓s,␈αand
␈↓ α∧␈↓there are other unexpected restrictions.

␈↓ α∧␈↓2.␈αThe␈αproperties␈αof␈αElephant␈αprograms␈αdon't␈αdepend␈αon␈αtime␈αtaking␈αinteger␈αvalues.␈α All␈αwe␈αneed
␈↓ α∧␈↓require␈αis␈αthat␈αthe␈αset␈αof␈αtimes␈αbe␈αordered␈αand␈αunbounded␈αabove.␈α Then␈αthe␈αfirst␈αsentence␈αof␈αthe
␈↓ α∧␈↓product program would take the form

␈↓ α∧␈↓␈↓↓∀t ∃t'.[t' > t ∧ i(t') ␈↓ βj= ␈↓ ∧∧IF pc(t) = 0 THEN n
␈↓ α∧␈↓↓␈↓ ∧∧ELSE IF pc(t) = 3 THEN i(t) - 1
␈↓ α∧␈↓↓␈↓ ∧∧ELSE i(t)].


␈↓ α∧␈↓This partial draft of ELEPHA[S79,JMC] compiled at 11:45 on April 6, 1979.